;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "mhipstafy.lisp")
(require "mhelpers.lisp")
(require "mhuechange.lisp")
(require "mbmptree.lisp")
(require "mavltree.lisp")
(require "mdatagenerators.lisp")

; Module responsible for testing the hipstafy module
(module THipstafy
  (import IHipstafy)
  (import iHueChange)
  (import iAvlTree)
  (import Ibmptree)
  (import iHelpers)
  (import Idatagenerators)
  
  (include-book "doublecheck" :dir :teachpacks) 
  (include-book "testing" :dir :teachpacks)
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; DATA GENERATORS
  ; Generates a random pixel (random RGB values).
  (defrandom random-pixel ()
    (let* ((r (random-between 0 255))
           (g (random-between 0 255))
           (b (random-between 0 255)))
      (list r g b)))
 
  ; Random bitmap file, uses a static header with a 
  ; size of heightxwidth.
  (defrandom random-bitmap (height width)
    (let* ((header (list 66 77 54 12 0 0 0 0 0 0 54 0 0 
                         0 40 0 0 0 width 0 0 0 height 0 0 0 1 
                         0 24 0 0 0 0 0 0 12 0 0 0 0 0 
                         0 0 0 0 0 0 0 0 0 0 0 0 0))
           (pixels (random-list-of (random-pixel) :size (* width height)))
           (tr (insert-header (empty-bmp-tree) header)))
      (fill-bitmap tr 0 0 height width pixels)))

  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; Check-expect tests
  
  (check-expect (hipstafy nil) nil)
  (check-expect (hipstafy (make-bmp-tree 
                           (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                       0 0 0 0 0 0 3 0 0 0 3)
                                 (list 0 0 (list 1 1 1)) 
                                 (list 0 1 (list 2 2 2))
                                 (list 0 2 (list 3 3 3)) 
                                 (list 1 0 (list 4 4 4))
                                 (list 1 1 (list 5 5 5)) 
                                 (list 1 2 (list 0 0 0))
                                 (list 2 0 (list 7 7 7)) 
                                 (list 2 1 (list 8 8 8))
                                 (list 2 2 (list 9 9 9)))))
                (list 4
                      1
                      (list 3 3 (list 4 4 4) (list 2 1 (list 5 5 5) (list 1 0 (list 4 4 4) nil nil) 
                                                   (list 1 2 (list 0 0 0) nil nil)) (list 2 4 (list 5 5 5) 
                                                   nil (list 1 5 (list 0 0 0) nil nil)))
                      (list 2
                            0
                            (list 3 3 (list 1 1 1) (list 2 1 (list 2 2 2) (list 1 0 (list 1 1 1) nil nil) 
                            (list 1 2 (list 3 3 3) nil nil)) (list 2 4 (list 2 2 2) nil (list 1 5 (list 3 3 3) nil nil)))
                            (list 1 -1 (list 1 -1 (list 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 6 0 0 0 6) nil nil) nil nil)
                            nil)
                      (list 3
                            3
                            (list 3 3 (list 1 1 1) (list 2 1 (list 2 2 2) (list 1 0 (list 1 1 1) nil nil) 
                           (list 1 2 (list 3 3 3) nil nil)) (list 2 4 (list 2 2 2) nil (list 1 5 (list 3 3 3) nil nil)))
                            (list 1 2 (list 3 3 (list 7 7 7) (list 2 1 (list 8 8 8) (list 1 0 (list 7 7 7) nil nil)
                            (list 1 2 (list 9 9 9) nil nil)) (list 2 4 (list 8 8 8) nil (list 1 5 (list 9 9 9) nil nil))) 
                            nil nil)
                            (list 2
                                  4
                                  (list 3 3 (list 4 4 4) (list 2 1 (list 5 5 5) (list 1 0 (list 4 4 4) nil nil)
                                  (list 1 2 (list 0 0 0) nil nil)) (list 2 4 (list 5 5 5) nil (list 1 5 (list 0 0 0)
                                                                                                    nil nil)))
                                  nil
                                  (list 1
                                        5
                                        (list 3 3 (list 7 7 7) (list 2 1 (list 8 8 8) (list 1 0 (list 7 7 7) nil nil) 
                                           (list 1 2 (list 9 9 9) nil nil)) (list 2 4 (list 8 8 8) nil (list 1 5 
                                          (list 9 9 9) nil nil)))
                                        nil
                                        nil)))))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; Property definitions
  
  ; verifies that hipstafy doubles the width and height
  (defproperty hipstafy-doubles-dimensions :repeat 10
    (oldtr :value (random-bitmap 10 10)
     newtr :value (hipstafy oldtr)
     neww :value (car (get-dimensions newtr))
     newh :value (cdr (get-dimensions newtr))
     oldw :value (car (get-dimensions oldtr))
     oldh :value (cdr (get-dimensions oldtr)))
     (and (equal neww (* 2 oldw)) (equal newh (* 2 oldh))))
 
  ; verifies that the hipstafy function returns a tree
  (defproperty hipstafy-returns-tree-prp :repeat 10
    (tr :value (random-bitmap 10 10))
    (bmp-tree? (hipstafy tr)))
  
  ; verifies that the hipstafy-helper function returns a tree
  ; (width height oldtree newtree xcurr xmax ycurr ymax)
  (defproperty hipstafy-helper-returns-tree-prp :repeat 10
    (oldtr :value (random-bitmap 10 10)
     width :value 10
     height :value 10
     newtr :value (insert-header (empty-bmp-tree) (get-header oldtr))
     xcurr :value 0
     ycurr :value 0
     xmax :value 10
     ymax :value 10)
    (bmp-tree? (hipstafy-helper width height oldtr newtr xcurr xmax ycurr ymax))))

(link RTHipstafy (Mavltree Mbmptree mDataGenerators mHelpers mHueChange MHipstafy THipstafy))
(invoke RTHipstafy)